[Zantema - RTA'97, Example 1]

Example 1 in [Zantema - RTA'97]

Summary: Ex1_Zan97

CS-TRS format
OBJ format
Negative results:
1. Lucas', Zantema's and Ferreira and Ribeiro's transformations
Positive results:

CS-TRS Ex1_Zan97 (file Ex1_Zan97.csr)

Functions:  g h c d

Constructors:  d

Variables:  X

Arities: 

ar(g) = 1
ar(h) = 1
ar(c) = 0
ar(d) = 0

Replacement map: 

µ(g)={}
µ(h)={}
µ(c)={}
µ(d)={}

Rules:  (file Ex1_Zan97) 
 
g(X) -> h(X)
c -> d
h(d) -> g(c)

The CS-TRS in OBJ format (file Ex1_Zan97.obj):

obj Ex1_Zan97 is
  sort S .
  op g : S -> S [strat (0)] .
  op h : S -> S [strat (0)] .
  op c : -> S .
  op d : -> S .
  vars X : S .
  eq g(X) = h(X) .
  eq c = d .
  eq h(d) = g(c) .
endo

Negative results

The µ-termination of Ex1_Zan97 cannot be proved terminating by either Lucas', Zantema's, or Ferreira and Ribeiro's transformations [GM99, Example 2, GM04, Example 16].

Positive results

The µ-termination of Ex1_Zan97 is proved in [Zan97, Example 1] by using the following interpretation:

    [c] = 2
    [d] = 1
    [g](x) = if x==1 then 4 else x
    [h](x) = if x==1 then 3 else x - 1

The µ-termination of Ex1_Zan97 is also proved in [GM04, Example 16] by using Giesl and Middeldorp's transformation. The TRS Ex1_Zan97_GM:

    a__g(X) -> a__h(X)
    a__c -> d
    a__h(d) -> a__g(c)
    mark(g(X)) -> a__g(X)
    mark(h(X)) -> a__h(X)
    mark(c) -> a__c
    mark(d) -> d
    a__g(X) -> g(X)
    a__h(X) -> h(X)
    a__c -> c

is terminating (use MuTerm).

The µ-termination of Ex1_Zan97 is also proved in [BLR02, Example 5] by using CSRPO and automatically by MuTerm.
The µ-termination of Ex1_Zan97 is proved in [Luc04, Example 2] by using a polynomial interpretation:
```
    [c] = 1
    [d] = 0
    [g](x) = x^2 - 3x + 4
    [h](x) = x^2 - 3x + 3
    
```
The µ-termination of Ex1_Zan97 can also be proved by using CSDP ( computed by MuTerm)